p,q:(n:  base-domain-type(n)). (eq_bd(p; q))  (p = q) 

latex

Definitions

top, True, T, x. t(x), P  Q, P  Q, P  Q, guard(T), sq_type(T), (i = j), bor(p; q), P  Q, base-domain-type(n), ff, prop{i:l}, P  Q, t  T, tt, t.2, if b then t else f fi , t.1, band(p; q), eq_bd(p; q), b, x:A. B(x), False, A, x(s), Unit, ,

Lemmas

equal-top, eq knd wf, assert-eq-knd, assert-eq-lnk, and functionality wrt iff, assert of band, bnot thru bor, true wf, squash wf, band wf, pi1 wf, pi2 wf, assert-eq-id, top wf, Knd wf, IdLnk wf, ifthenelse wf, Id wf, eq id wf, iff functionality wrt iff, or functionality wrt iff, assert of bor, bor wf, base-domain-type wf, not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, assert of eq int, eqtt to assert, assert wf, iff transitivity, bool wf, eq int wf